Nuprl Lemma : map-map
0,22
postcript
pdf
as
:Top List,
f
,
g
:Top. map(
g
;map(
f
;
as
)) ~ map(
g
o
f
;
as
)
latex
Definitions
Top
,
x
:
A
.
B
(
x
)
,
t
T
Lemmas
top
wf
origin
as:Top List, f, g:Top. map(g;map(f;as)) ~ map(g o f;as) as:Top List, f, g:Top. map(g;map(f;as)) ~ map(g o f;as) x:A. B(x)
T